Problem:
 and(tt(),X) -> activate(X)
 plus(N,0()) -> N
 plus(N,s(M)) -> s(plus(N,M))
 activate(X) -> X

Proof:
 Bounds Processor:
  bound: 1
  enrichment: match
  automaton:
   final states: {6,5,4}
   transitions:
    s1(7) -> 7,5
    plus1(3,1) -> 7*
    plus1(3,3) -> 7*
    plus1(1,2) -> 7*
    plus1(2,1) -> 7*
    plus1(2,3) -> 7*
    plus1(3,2) -> 7*
    plus1(1,1) -> 7*
    plus1(1,3) -> 7*
    plus1(2,2) -> 7*
    activate1(2) -> 4*
    activate1(1) -> 4*
    activate1(3) -> 4*
    and0(3,1) -> 4*
    and0(3,3) -> 4*
    and0(1,2) -> 4*
    and0(2,1) -> 4*
    and0(2,3) -> 4*
    and0(3,2) -> 4*
    and0(1,1) -> 4*
    and0(1,3) -> 4*
    and0(2,2) -> 4*
    tt0() -> 1*
    activate0(2) -> 6*
    activate0(1) -> 6*
    activate0(3) -> 6*
    plus0(3,1) -> 5*
    plus0(3,3) -> 5*
    plus0(1,2) -> 5*
    plus0(2,1) -> 5*
    plus0(2,3) -> 5*
    plus0(3,2) -> 5*
    plus0(1,1) -> 5*
    plus0(1,3) -> 5*
    plus0(2,2) -> 5*
    00() -> 2*
    s0(2) -> 3*
    s0(1) -> 3*
    s0(3) -> 3*
    1 -> 4,7,6,5
    2 -> 4,7,6,5
    3 -> 4,7,6,5
  problem:
   
  Qed